This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation systems and arithmetic operations/formulae). Using ARITH, we can provide formal description of arithmetic algorithms including those using unconventional number systems. In addition, the described arithmetic algorithms can be formally verified by equivalence checking with formula manipulations. The verified ARITH descriptions are easily translated into the equivalent HDL descriptions. In this paper, we also present an application of ARITH to an arithmetic module generator, which supports a variety of hardware algorithms for 2-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The language processing system of ARITH incorporated in the generator verifies the correctness of ARITH descriptions in a formal method. As a result, we can obtain highly-reliable arithmetic modules whose functions are completely verified at the algorithm level.

We introduce PC Linux cluster computing techniques to an Evolutionary Graph Generation (EGG) system, and successfully implement the parallel version of the EGG system, called PEGG. Our survey satisfactorily shows that the parallel evolutionary approach meets our expectation that the final solutions obtained from PEGG will be as good as or better than those obtained from EGG, and that PEGG can ultimately improve the speed of evolution.

This paper presents an algorithm-level interpretation of fast adder structures in binary/multiple-valued logic. The key idea is to employ a unified representation of addition algorithms called Counter Tree Diagrams (CTDs). The use of CTDs makes it possible to describe and analyze addition algorithms at various levels of abstraction. A high-level CTD represents a network of coarse-grained components associated with multiple-valued logic devices, while a low-level CTD represents a network of primitive components directly mapped onto binary logic devices. The level of abstraction in circuit representation can be changed by decomposition of CTDs. We can derive possible variations of adder structures by decomposing a high-level CTD into low-level CTDs. This paper demonstrates the interpretation of redundant arithmetic adders based on CTDs. We first introduce an extension of CTDs to represent possible redundant arithmetic adders with limited carry propagation. Using the extended version of CTDs, we can classify the conventional adder structures including those using emerging devices into three types in a systematic way.